i:Id, A:MsgA. @i: A  IdMsgA 

latex

Definitions	x:A. B(x), t  T, @i: A, if b then t else f fi , P  Q, tt, , ff, , Unit, P  Q, P & Q,
Lemmas	eq id wf, bool wf, iff transitivity, assert wf, Id wf, eqtt to assert, assert-eq-id, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, ma-empty wf, msga wf